\documentclass[12pt]{article}
\usepackage{fullpage,cmu-titlepage2}
\usepackage{times}
\usepackage{excludeonly}

\usepackage[T1]{fontenc}

\usepackage{amssymb}
\usepackage{listings}
\usepackage{mathpartir}
\usepackage{graphicx}
\usepackage{tabularx}
\usepackage[release]{PlaidDefinitions}
\usepackage{datetime}
\usepackage{natbib}

\newcommand{\singlespace}{\renewcommand{\baselinestretch}{1.0}\normalsize}

\renewcommand{\cite}{\citep}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{The Plaid Language:\\
Typed Core Specification\\
\vspace{2ex}
version 0.4.0\\
\vspace{2ex}
}

\author{Jonathan Aldrich \and Nels E. Beckman \and Robert Bocchino \and Karl Naden \and Darpan Saini \and Sven Stork \and Joshua Sunshine}


\date{\monthname~\the \year}

\abstract{
Plaid is an object oriented programming language built on two paradigms.  First, Plaid
is {\it typestate-oriented}. Programmers can directly encode the {\it abstract states}
of objects and use the {\it state change operator} to change the state, interface, and representation
of an object at runtime.  Second, Plaid's type system is {\it permission-based}.  The type of each reference 
includes an {\it access permission} which dictates how the reference can be used and characterizes
the permissions to other aliases of the same object.  Plaid leverages permissions 
when tracking the abstract state of references during typechecking.  Permissions are
also used to infer code that can be safely run in parallel.
This document defines the core of the Plaid language, including its source syntax, 
the semantics of operations involving abstract states, and a type system.
}





\keywords{programming language, typestate, Plaid, gradual typing, permissions}

\trnumber{CMU-ISR-12-103}


\support{This research was supported by DARPA grant HR00110710019, CMU|Portugal Aeminium grant CMU-PT/SE/0038/2008, NSF grants CCF-0811592 and CCF-1116907, and grant \#1019343 to the Computing Research Association for the
CIFellows Project.}


\begin{document}

\renewcommand*{\thepage}{title-\arabic{page}} 
\maketitle
\renewcommand*{\thepage}{\arabic{page}} 




%%%%%%%%%%%%%%%%%%%% MAIN TEXT %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\input{conventions}

\input{lexing}

\input{expressions}

\include{types}

\input{compilation-units}

\bibliographystyle{plainnat}
\bibliography{spec}


\end{document}
